

(defun make-exp (op &rest args) (cons op args))
(defun op (exp) "Operator of an expression" (if (listp exp) (first exp) exp))
(defun args (exp) "Arguments of an expression" (if (listp exp) (rest exp) nil))
(defun arg1 (exp) "First argument" (first (args exp)))
(defun arg2 (exp) "Second argument" (second (args exp)))



(defun last1 (list)
  "Return Last Item"
  (first (last list)))

(defun length=1? (list)
  "List of 1 element?"
  (and (consp list) (null (cdr list))))

(defun len>1? (list)
  "Is this a list of 2 or more elements?"
  (and (consp list) (cdr list)))

(defun stringify (exp)
  "Coerce argument to a string."
  (cond ((stringp exp) exp)
    ((symbolp exp) (symbol-name exp))
    (t (format nil "~A" exp))))

(defun numeric-string-p (string)
  (let ((*read-eval* nil))
    (ignore-errors (numberp (read-from-string string)))))


(defun get-length (x)
  (let ((retval nil))
    (setf retval (ignore-errors (length x)))
    (if (eq retval nil)
      0
      retval)))


(defun case? (s)
  "Determins if the s is all LowerCase or Uppercase"
  ;(write-line (format nil "S Value is: ~a" s))
  (let ((isLower nil) (isUpper nil) (isANum nil) (hasNum nil) (letterfirst nil) (letterlast nil))
    ;All Numbers
    (if (every #'numberp s)
        (write-line (format nil "AllNum!")))
    ;Starts with Letter/Number
    (if (alpha-char-p (char s 0))
        ;(write-line (format nil "Starts with Letter")
        (setf letterfirst t))
        ;(write-line (format nil "Starts with Number")))
    ;Ends with Letter/Number
    (if (alpha-char-p (char s (- (length s) 1)))
        ;(write-line (format nil "Ends with Letter") 
        (setf letterlast t))
        ;(write-line (format nil "Ends with Number"))
    (loop for x from 0 to (1- (length s)) do
      (if (lower-case-p (char s x))
        (setq isLower t)
        (setq isUpper t))
      (if (ALPHANUMERICP (char s x))
        (setq isANum t))
      (if (numeric-string-p (stringify (char s x)))
        (setq hasNum t))
    )
  ;(write-line (format nil "Alph: ~a" isANum))
  ;(write-line (format nil "Up: ~a" isUpper))
  ;(write-line (format nil "Low: ~a" isLower))
  ;(write-line (format nil "HasNum: ~a" hasNum))
  (cond 
    ((eq hasNum t)
      (if (and hasNum letterfirst (eq letterlast nil) (eq isLower nil) (eq isUpper t))
        ;(write-line (format nil "OK"))
        (setq s T)
        ;(write-line (format nil "Bad!~A" isUpper))
        (setq s nil)
       ))
        
    ((eq hasNum nil)
      ;(if (and isUpper isANum (alpha-char-p (char s 0)) (eq isLower nil) (eq isLower nil))
      (if (and isUpper isANum (alpha-char-p (char s 0)) ) 
        (setq s T)))
   )))


(defun wfp-listp (wfps)
  "Helper function for wfp-checker to check the syntax on the well formed proposition"
  (dolist (wfp wfps)
    (unless (wfp-checker wfp)
      (return-from wfp-listp nil)))
    t)

(defun wfp-checker (wfp)
  "Checks to see if the argument is a correct well formed proposition."
  ;(write-line  (format nil "sentence:~a" wfp))
  (if (atom wfp)  nil           ; means its a proposition
    ;(if (and (atom wfp)(listp wfp))  t           ; means its a proposition
    (case (car wfp)               ; else check whether its a particular type of wfp
      ;==========================================
      ((or and) ;conjunction/disjunction
       (wfp-listp (cdr wfp)))    ; check if each of its arguments is a wfp
      ;==========================================
      (not  ;;negated
        (if (= (length wfp) 2)
          (wfp-checker (second wfp))
          nil))
      ;==========================================
      ((implies iff) ; implications
       (if (= (length wfp) 3)
         (wfp-listp (cdr wfp))
         nil))
      ;==========================================
      ;((EQUIV iff) ; Equivalences
      (EQUIV  ; Equivalences
        (if (= (length wfp) 3)
          (wfp-listp (cdr wfp))
          nil))
      ;==========================================
      (otherwise            ; its a proposition
        ;; But make sure that the first element of the proposition is an
        ;; atom.  We do not support lists as the predicate name
;        (write-line (format nil "Length: ~a" (length  wfp)))
;        (write-line  (format nil "wfp: ~a" wfp))
;        (write-line  (format nil "listp ~a" (listp wfp)))
;        (write-line  (format nil "case: ~a" (case? (stringify wfp))))
;        (write-line  (format nil "car wfp: ~a" (car wfp)))
        (cond
          ((len>1? wfp)   ; Length of wfp is too Long
            ;(write-line  (format nil "Too Long!-t:~a -- NIL" (car wfp)))
            nil
          )

          ((eq (listp wfp) nil) ; does not have paren's around pred
            ;(write-line  (format nil "listp-f:~a" (car wfp)))
            nil
          )
            
          ((and (eq (atom (car wfp)) t) (eq (listp wfp) t) (eq (case? (stringify (car wfp))) t))
            t
          )
        )
))))


(defun TruthValue (sentence &optional interpretation)
  "Evaluate the truth of the sentence under an interpretation.
  The interpretation is a list of (proposition . truth-value) pairs,
  where a truth-value is t or nil, e.g., ((P . t) (Q . nil)).
  It is an error if there are any propositional symbols in the sentence
  that are not given a value in the interpretation."
  ;(let ((truthval (sublis interpretation sentence))) 
;  (write-line (format nil "StartOf TruthValue" ))
;  (write-line (format nil "interpre: ~a" interpretation))
;  (write-line (format nil "sentence ~a" sentence))
;  (write-line (format nil "ops ~a" (op sentence)))
;  (write-line (format nil "intops ~a" (op interpretation)))
;  (write-line (format nil "sublis: ~a" (sublis sentence interpretation )))
;  (write-line (format nil "truthval: ~a" truthval))
;  (write-line (format nil "============================"))
;  (write-line (format nil "operand ~a" (op sentence)))
;  (write-line (format nil "opercar ~a" (op (car sentence))))
;  (write-line (format nil "============================"))
  (cond 
    (interpretation (TruthValue (sublis interpretation sentence ) nil))
    ;((eq sentence 'true) t)
    ((eq (op (car sentence)) t) t)
    ;((eq (op (car sentence)) 'true) t)
    
    ;((eq sentence 'false) nil)
    ((eq (op (car sentence)) nil) 
       ;(write-line (format nil "FALSE!"))
       nil)
    ((atom sentence) (error "No interpretation for ~A." sentence))
    (t 
     
     (case (op (car sentence))
       (or  (some #'TruthValue (args sentence)))
       (and 
         ;(write-line (format nil "AND!")) 
         (every #'TruthValue (args sentence))
         ;(every #'TruthValue (args truthval))
       )
       (NOT 
;        (write-line (format nil "NOT! --~a" (arg1 sentence)))
        (not (TruthValue (arg1 sentence)))
       )
       (IMPLIES  (or (TruthValue (arg2 sentence))
         (not (TruthValue (arg1 sentence)))))
       (EQUIV (eq (TruthValue (arg1 sentence))
         (TruthValue (arg2 sentence))))
       (otherwise 
         (error "Unknown connective ~A in ~A" (op sentence) sentence)
         ;(write-line (format nil "ERROR!! Unknown connective ~A in ~A" (op sentence) sentence))
         nil
       )))
    ))


(defun IsTautology (clause)
  "Is clause a tautology (something that is always true)?"
  (let ((taut (some #'(lambda (literal)
        (and (eq (op literal) 'not)
         (member (arg1 literal) clause :test #'equal)))
    clause)))
  ;(if (not (eq bob t)) (write-line (format nil "return: ~a" bob)))
  (if (not (eq taut nil)) t)
  ))


(defun wfp-FOL-listp (wfps)
  "Helper function for wfp-checker to check the syntax on the well formed proposition"
  (write-line (format nil "wfp-FOL-listp Len ~a" (length  wfps)))
  (dolist (wfp wfps)
    (unless (wfp-checkerFOL wfp)
      (return-from wfp-listp nil)))
    t)

(defun wfp-checkerFOL (wfp)
  "Checks to see if the argument is a correct well formed proposition."
;  (write-line (format nil "----------------------------" ))
;  (write-line  (format nil "sentence:~a" wfp))
;  (write-line (format nil "Length: ~a" (length  wfp)))
;  (write-line (format nil "Before hand-quant: ~a" wfp))
  (setf wfp (handle-quantifiers wfp))
;  (write-line (format nil "After hand-quant: ~a" wfp))
;  (write-line (format nil "============================"))
;  (write-line  (format nil "wfp:     ~a" wfp ))
;  (write-line  (format nil "op      : ~a" (op wfp)))
;  (write-line  (format nil "car     : ~a  : ~a" (get-length (car wfp)) (car wfp) ))
;  (write-line  (format nil "cdr     : ~a  : ~a" (get-length (cdr wfp)) (cdr wfp) ))
;  (write-line  (format nil "arg1    : ~a  : ~a" (get-length (arg1 wfp)) (arg1 wfp) ))
;  (write-line  (format nil "arg2    : ~a  : ~a" (get-length (arg2 wfp)) (arg2 wfp) ))
;  (write-line  (format nil "second  : ~a  : ~a" (get-length (second wfp)) (second wfp) ))
  
;  (write-line (format nil "============================"))
;  (if (atom wfp)  
;    (write-line (format nil "Atom-wfp: ~a" wfp) (nil))           ; means its a proposition
    (case (car wfp)               ; else check whether its a particular type of wfp
      ;==========================================
      ((or and) ;conjunction/disjunction
;        (write-line  (format nil "Or Condition:~a -- NIL" wfp))
        (wfp-FOL-listp (cdr wfp)))    ; check if each of its arguments is a wfp
      ;==========================================
      (not  ;;negated
;        (write-line  (format nil "NOT Condition:~a -- NIL" wfp))
        (if (= (length wfp) 2)
          (wfp-checkerFOL (second wfp))
          nil))
      ;==========================================
      ((IMPLIES) ; implications
;        (write-line  (format nil "IMPLIES Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ;((EQUIV iff) ; Equivalences
      (EQUIV  ; Equivalences
;        (write-line  (format nil "EQUIV Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ((ALL) ; implications
;        (write-line  (format nil "ALL Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      ((EXISTS) ; implications
;        (write-line  (format nil "EXISTS Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)
          (wfp-FOL-listp (cdr wfp))
          nil))
      ;==========================================
      (otherwise
        (cond
          ;==========================================
          ;; PREDICATE
          ((eq (predicatep (stringify (op wfp))) t)
          ;((eq (predicatep (stringify (arg1 wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "PREDICATE???: ~a   len: ~a" (op wfp) (get-length wfp)))
            (if (> (get-length wfp) 1)
              ;(wfp-FOL-listp (arg1 wfp))
              (wfp-checkerFOL (cdr wfp))
              t))
          ;==========================================
          ;;TERM
          ((eq (termp (stringify (op wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "TERM!: ~a of ~a   len: ~a" (op wfp) (arg1 wfp) (get-length wfp)))
;            (write-line  (format nil "Result: ~a" (termp (stringify (op wfp)))))
            (if (termp (stringify (op wfp)))
              (cond 
                ( (= (get-length wfp) 1)
                  ;(write-line  (format nil "~a is a term" (car wfp))))
                  t)
                ( (> (get-length wfp) 1)
                  ;(wfp-FOL-listp (cdr wfp))))
                  (wfp-checkerFOL (cdr wfp)))
                (t
                  (write-line  (format nil "Something Funny Happened")))
                  ;nil)
              )
              ;(write-line  (format nil "~a is NOT a term" (car wfp))))
              nil)
          )
          
          ;==========================================
          ;; FUNCTION
          ((eq (funcp (stringify (op wfp))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "FUNCTION! ~a of ~a" (op wfp) wfp))
            (if (> (get-length wfp) 1)
              ;(wfp-FOL-listp (cdr wfp))
              ;(wfp-checkerFOL (cdr wfp))
              (wfp-checkerFOL (cdr wfp))
              ;wfp-FOL-listp (cdr wfp))
              nil))
          
          ;==========================================
          ;; NESTED PREDICATE
          ((eq (predicatep (stringify (car (op wfp)))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "NESTED PREDICATE!! :~a of ~a" (op wfp) wfp))
            (wfp-checkerFOL (car wfp))
            
           )
          
          ;==========================================
          ;; NESTED FUNCTION
          ((eq (funcp (stringify (car (op wfp)))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "NESTED FUNCTION! :~a of ~a" (op wfp) wfp))
            (wfp-checkerFOL (car wfp))
            
           )
          
          ;==========================================
          ;; NESTED TERM
          ((eq (termp (stringify (car (op wfp)))) t)
;            (write-line (format nil "____________________"))
;            (write-line  (format nil "NESTED TERM :~a of ~a" (op wfp) wfp))
            (wfp-checkerFOL (car wfp))
            
           )
          ;==========================================
          ((and (eq (atom (car wfp)) t) (eq (listp wfp) t) (eq (case? (stringify (car wfp))) t))
            t
          )
        )
)))

(defun handle-quantifiers (exp)
  "Change (ALL x y P) to (ALL (x y) P)."
  (if (member (op exp) '(ALL EXISTS))
    `(,(op exp) ,(butlast (rest exp)) ,(last1 exp))
    exp))


(defun term-type (s)
  (let (
        (strlen (if (equal (length s) 1) t))
        (isLower (lower-case-p (char s 0))) 
        (isUpper (upper-case-p (char s 0))))
  (cond
    ((and strlen isUpper (case? (stringify (char s 0))))
      (print"predicate"))
    ;((and strlen isLower (if (search s "abcdeuvwxyz") t nil))
    ;  (print"term"))
    ((and strlen isLower (if (search s "abcde") t nil))
      (print"constant"))
    ((and strlen isLower (if (search s "fgh") t nil))
      (print"symbols"))
    ((and strlen isLower (if (search s "uvwxyz") t nil))
      (print"variables"))
    (t 
       nil
))))

(defun termp (s)
;  (write-line  (format nil "s=~a" s))
  (cond
    ((and (if (equal (length s) 1) t) (lower-case-p (char s 0)) (if (search s "abcde") t nil))
      t)
    ((and (if (equal (length s) 1) t) (lower-case-p (char s 0)) (if (search s "uvwxyz") t nil))
      t)
    (t 
       nil
)))
(defun funcp (s)
  (cond
    ((and (if (equal (length s) 1) t) (lower-case-p (char s 0)) (if (search s "fgh") t nil))
      t)
    (t 
       nil
)))

(defun predicatep (s)
  (cond
    ((and (if (equal (length s) 1) t) (upper-case-p (char s 0)) (case? (stringify (char s 0))))
      t)
    (t 
       nil
)))





(defun testfun () 
  ;Should Fail


 ;Should Succeed

  (and nil nil)
  (not nil)
  (not t)
)